COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	(wipe-out) 
C00010 ENDMK
C⊗;
(wipe-out) 
(proof lispax) 

;;;declarations: note that t and nil are not declared - ekl knows about them
;;;since they are attached, we don't need to say things like null nil etc.

(decl car (unaryname: car) (type: |ground→ground|) (syntype: constant)
 (bindingpower: 950))

(decl cdr (unaryname: cdr) (type: |ground→ground|) (syntype: constant)
 (bindingpower: 950))

(decl atom (unaryname: atom) (type: |ground→truthval|) (syntype: constant)
 (bindingpower: 750))

(decl null (unaryname: null) (type: |ground→truthval|) (syntype: constant)
 (bindingpower: 750))

(decl listp (unaryname: listp) (type: |ground→truthval|) (syntype: constant)
 (bindingpower: 750))

(decl alistp (unaryname: alistp) (type: |ground→truthval|) (syntype: constant)
 (bindingpower: 750))

(decl sexp (unaryname: sexp) (type: |ground→truthval|) (syntype: constant)
 (bindingpower: 750))

(decl (u v w) (type: |ground|) (sort: |listp|))

(decl (x y z) (type: |ground|) (sort: |sexp|))

(decl (xa ya za) (type: |ground|) (sort: |atom|))

(decl (a b c) (type: |ground|))

(decl (phi) (type: |ground→truthval|))

(decl cons (type: |(ground⊗ground)→ground|) (syntype: constant) (infixname: |.|)
 (prefixname: cons) (bindingpower: 850))

;;;basic axioms and sort info

(axiom |∀xa.sexp(xa)|)
(label simpinfo)

(axiom |∀u.sexp u|)
(label simpinfo)

(axiom |∀x u.listp x.u|)
(label simpinfo)

(axiom |∀u.¬null u ⊃ listp cdr u|)
(label simpinfo)

(axiom |∀u.¬null u ⊃ sexp car u|)
(label simpinfo)

(axiom |∀x.¬atom x ⊃ sexp car x|)
(label simpinfo)

(axiom |∀x.¬atom x ⊃ sexp cdr x|)
(label simpinfo)

(axiom |∀x y.sexp x.y|)
(label simpinfo)

(axiom |∀x y.¬atom x.y|)
(label simpinfo)

(axiom |∀x u.¬null x.u|)
(label simpinfo)

(axiom |∀u.null u ⊃ u = nil|)
(label simpinfo)

(axiom |∀x y.car (x.y) = x|)
(label simpinfo)

(axiom |∀x y.cdr (x.y) = y|)
(label simpinfo)

(axiom |∀u.¬null u ⊃ (car u.cdr u=u)|)
(label simpinfo)

(axiom |∀x.¬atom x ⊃ (car x.cdr x=x)|)
(label simpinfo)

;;;induction

(axiom |∀phi.phi(nil)∧(∀x u.phi(u)⊃phi(x.u))⊃(∀u.phi(u))|)
(label listinduction)

(decl pars (type: |ground*|))
(decl (df df1 df2) (type: |ground⊗ground*→ground*|))
(decl nilcase (type: |ground*→ground*|))
(axiom
 |∀df nilcase def.(∃fun.(∀pars x u.fun(nil,pars)=nilcase(pars)∧
	             		   fun(x.u,pars)=def(x,u,fun(u,df(x,pars)),pars)))|)
(label listinductiondef)

(axiom |∀phi.(∀x.atom x ⊃ phi(x))∧(∀x y.phi(x)∧phi(y)⊃phi(x.y))⊃(∀x.phi(x))|)
(label sexpinduction)

(axiom
 |∀atomcase defsexp df1 df2.
   ∃fun. ∀pars x y.
    (atom x ⊃ fun(x,pars)=atomcase(x,pars))∧
    (fun(x.y,pars)=defsexp(x,y,fun(x,df1(x,pars)),fun(y,df2(x,pars)),pars))|)
(label sexpinductiondef)

;;; lists of variable numbers of arguments don't require special treatment,
;;; since we have list types now

(decl list (type: |ground* → ground|) (syntype: constant))
(decl lst (type: |ground*|))

(axiom |list() = nil|)
(label simpinfo)

(axiom |∀lst.listp(list(lst))|)
(label simpinfo)

(axiom |∀x lst.list(x,lst) = x.list(lst)|)
(label simpinfo)
(label listdef)

;;; this is lisp's append.  while it can be proved associative, it
;;; is convenient in proofs of other theorems to have it declared
;;; associative.
 
(decl append (type: |ground⊗ground⊗(ground*)→ground|) (syntype: constant)
      (associativity: both) (infixname: *) (bindingpower: 840))

(defax append |∀x u v.nil*v=v∧(x.u)*v=x.(u*v)|)
(label appendef) (label simpinfo)

(axiom |∀u v.listp(u*v)|)
(label simpinfo) (label listappend)

(axiom |∀u.u*nil=u|)
(label simpinfo)

(axiom |∀x v.(x.nil)*v=x.v|)
(label simpinfo)

;;;map functions on lists

(decl (allp somep) (syntype: constant) (type: |(@phi)⊗ground→truthval|))
(defax allp |∀phi x u.allp(phi,nil)∧
       		      allp(phi,x.u)=if phi(x) then allp(phi,u) else false|)
(label allpdef)

(defax somep |∀phi x u.¬somep(phi,nil)∧
       		       somep(phi,x.u)=if phi(x) then true else somep(phi,u)|)
(label somepdef)

(defax mapcar |∀fn x u.mapcar(fn,nil)=nil∧mapcar(fn,x.u)=fn(x).mapcar(fn,u)|)
(label mapcardef)

(decl (alist a0 a1 a2) (type: ground) (sort: alistp))
(axiom |∀alist. listp alist|)
(label simpinfo) 

(axiom |∀alist. ¬null alist ⊃ ¬atom car alist ∧ atom car car alist|)

(axiom |∀xa y alist.alistp (xa.y).alist|)
(label mkalist)

(decl assoc (type:  |ground⊗ground → ground|) (syntype: constant))

(defax assoc |∀x xa y alist.
              assoc(x,nil)=nil∧
              assoc(x,(xa.y).alist)=(if x=xa then xa.y else assoc(x,alist))|)
(label assocdef)

(axiom |∀x alist.sexp assoc(x,alist)|)
(label simpinfo)

(decl member (type: |ground⊗ground → truthval|) (syntype: constant))

(defax member |∀x y u. ¬member(x,nil)∧member(x,y.u)=(x=y∨member(x,u))|)
(label memberdef)
(save-proofs lispax)